/**
 * Class to handle formulas
 * Includes functions to combine and transform formulas
 * TODO: add syntax
 * Used in all the parser 
 * @see parser....
 */

package chameleon.model.formula;

import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.utils.Node;
import com.sun.jna.Pointer;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Hashtable;

/**
 * This class represent a formula. This class has a tree structure. 
 * 
 * It is possible to create "at hand" a formula by using the different constructor.
 * 
 * Or you can use the following parser : 
 *   -@parser.LtlParser that creates an LTL formula
 *   -@parser.BooleanParser that creates a boolean expression
 *   -@parser.MathematicalParser that creates a mathematical expression.
 *
 * The general syntax is :
 *
 * f :: true | false | UnaryOp f | f BinaryOp |
 *
 * More specific syntax are defined in parser classes.
 *
 * This classes do also a link between NuGat and Chameleon. The method encFormula
 * computes and return the NuGat node representation for the formula.
 *
 *
 * @author simon
 */
public class Formula {

    private Formula rightFormula_;
    private Formula leftFormula_;
    private Operator operator_;
    private boolean isAtomic_;
    //represent the atomic propsisition true or false, not the valuation of formula
    private boolean isTrue_;
    private boolean isFalse_;
    private String proposition_;
    private int numVar_;
    private int nbreVar_;
    private boolean isInteger_;
    private NuGatInterface nugat_;
    private Hashtable smvMapTable_;

    //************************* CONSTRUCTOR ******************************//

    public Formula(){
        initBool();
    }
    
    /**
     * Construction of an atomic formula.
     * @param proposition
     */

    public Formula (String proposition){
        proposition_ = proposition;
        isAtomic_ = true;
        initBool();
        isInteger_ = isInteger(proposition);
        if (proposition_.equals("True") || proposition_.equals("true")){
            isTrue_ = true;
        }
        else if (proposition_.equals("False") || proposition_.equals("false")){
            isFalse_ = true;
        }
    }

    /**
     * Construction of a formula with unary operator.
     * @param rightFormula
     * @param op
     */

    public Formula (Formula rightFormula, Operator op){
        rightFormula_ = rightFormula;
        operator_ = op;
        isAtomic_ = false;
        initBool();
    }

    /**
     * Construction of a formula with bnary operator.
     * @param left
     * @param right
     * @param op
     */

    public Formula (Formula left, Formula right, Operator op){
        leftFormula_ = left;
        rightFormula_ = right;
        operator_ = op;
        initBool();
    }

    /**
     * copy constructor
     * @param formula
     * @throws IOException
     */

    public Formula (Formula formula) {
        rightFormula_ = formula.getRightF();
        leftFormula_ = formula.getLeftF();
        operator_ = formula.getOperator();
        isAtomic_ = formula.isAtomic();
        isTrue_ = formula.isTrue();
        isFalse_ = formula.isFalse();
        proposition_ = formula.toString();
    }

    private void initBool(){
        isFalse_ = false;
        isTrue_ = false;
    }

    //*********************** GETTER ******************************//

    public Formula getRightF(){
        if (rightFormula_ != null)
            return rightFormula_;
        else
            return null;
    }

    public Formula getLeftF() {
        if (leftFormula_ != null)
            return leftFormula_;
        else
            return null;
    }

    public Operator getOperator() {
        if (operator_ != null)
            return operator_;
        else
            return null;
    }

    @Override
    public String toString(){
            return runFormula(Tag.STRING);
    }

    private String toCnfString() {
        return runFormula(Tag.CNF_STRING);
    }


    /**
     * This method explore formula and this behavior change in function of
     * action parameter.
     *
     * @param action
     * @return
     * @throws IOException
     */

    private String runFormula(int action) {
         //Atomical proposition
        if (isAtomic_){
            if (action == Tag.STRING)
                return proposition_;
            else if (action == Tag.CNF_STRING)
                return numVar_+" ";
            else
                throw new RuntimeException("Formula::Unknow action");
        }
        //Unary operator
        else if(leftFormula_ == null){
            if (action == Tag.STRING){
                if (operator_.getTag() == Tag.NEXT_TRANSITION)
                    return "("+operator_.toString()+"("+rightFormula_.toString()+")"+")";
                else
                    return "("+operator_.toString()+" "+rightFormula_.toString()+")";
            }
            else if (action == Tag.CNF_STRING){
                if (operator_.getTag()==Tag.NOT)
                    return "-"+rightFormula_.toCnfString();
                else
                    return rightFormula_.toCnfString();
            }
            else
                throw new RuntimeException("Formula::Unknow action");
        }
        //Classical formula
        else
            if (action == Tag.STRING)
                return"("+leftFormula_.toString()+" "+operator_.toString()+" "+
                    rightFormula_.toString()+")";
            else if (action == Tag.CNF_STRING){
                return leftFormula_.toCnfString()+" "+rightFormula_.toCnfString();
            }
            else
                throw new RuntimeException("Formula::Unknow action");
    }

    public int getNbreVar(){
        return nbreVar_;
    }
    
    public int getNbreClauses(){
        if (isCNF()){
            /**
             * As we have a CNF formula we are sure than the left part of the
             * formula is a clause. The question is is the right part a clause
             * too?
             */
            if (isAtomic_)
                return 1;
            else if(rightFormula_.isOrFormula())
                if (isOrFormula())
                    return 1;
                else
                    return 2;
            else
                return 1 + rightFormula_.getNbreClauses();
        }
        else
            return -1;
    }

    @Override
    public Formula clone(){
            return new Formula(this);
    }

    //*********************** SETTER *******************************//
    
    public void setNugatInterface (NuGatInterface nugat){
        nugat_ = nugat;
    }
    
    public void setSmvMapTable (Hashtable smvMapTable){
        smvMapTable_ = smvMapTable;
    }

    //*********************** QUESTION METHOD **********************//

    private boolean isInteger(String prop){
        char[] proposition = prop.toCharArray();
        for (int i=0; i < proposition.length; ++i ){
            int nbre = proposition[i]-'0';
            if (!(nbre >=0 && nbre <= 9))
                return false;
        }
        return true;
    }

    public boolean isInteger(){
        return isInteger_;
    }

    public boolean isAtomic(){
        return isAtomic_;
    }

    /**
     * Return true, if the formula is the atomic proposition true;
     * @return
     */

    public boolean isTrue(){
        return isTrue_;
    }

    /**
     * Return true if the formula is the atomic proposition false;
     * @return
     */

    public boolean isFalse(){
        return isFalse_;
    }

    public boolean isCNF(){
        if (isAtomic_ || (operator_.getTag()==Tag.NOT && rightFormula_.isAtomic_))
            return true;
        else if(operator_.getTag() == Tag.AND)
            return leftFormula_.isCNF() && rightFormula_.isCNF();
        else if (operator_.getTag() == Tag.OR)
            return leftFormula_.isOrFormula() && rightFormula_.isOrFormula();
        else
            return false;
    }

    public boolean isOrFormula(){
        //An or formula is a formula of the form : a||b||!c
        if (isAtomic_)
            return true;
        else if (operator_.getTag()==Tag.OR)
            return leftFormula_.isOrFormula() && rightFormula_.isOrFormula();
        else if (operator_.getTag()==Tag.NOT)
            return rightFormula_.isOrFormula();
        else
            return false;
    }
    
    /**
     * A sat formula is a formula without temporal operator.
     * @return 
     */
    
    public boolean isSatFormula(){
        if (isAtomic_)
            return true;
        else if (!operator_.isTemporal())
            if (operator_.isUnary())
                return rightFormula_.isSatFormula();
            else
                return leftFormula_.isSatFormula() && rightFormula_.isSatFormula();
        else
            return false;
    }

    public boolean isEquals (Formula formula) {

        if (isAtomic()){
            if (formula.isAtomic())
                return proposition_.equals(formula.toString());
            else
                return false;
        }

        //Unary formula

        else if (leftFormula_ == null){
            if(formula.getLeftF() == null && formula.getRightF()!=null
                    && !formula.isAtomic()){
                return (operator_.isEquals(formula.getOperator().getTag())
                        && rightFormula_.isEquals(formula.getRightF()));
            }
            else
                return false;

        }

        //Binary formula

        else{
            if(formula.getLeftF() != null && formula.getRightF()!=null
                    && !formula.isAtomic()){
                return (operator_.isEquals(formula.getOperator().getTag())
                        && rightFormula_.isEquals(formula.getRightF())
                        && leftFormula_.isEquals(formula.getLeftF()));

            }
            else
                return false;


        }

    }

    //*********************** TRANSFORMATION METHOD ****************//

    //Convert this formula to the CNF equivalent formula
    public void convert2CNF() {
        if (isSatFormula()){
            if (!isCNF()){
                /**
                 * First step of the algorith :
                 *  Delete all the -> and <-> operator
                 * (a->b) = (!a||b)
                 * (a<->b) = (!a||b)&&(a||!b)
                 */
                removeImpEqu();

                /**
                 * Second step of the algorithm :
                 *  enther the negatives as possible inside
                 * !(a&&b) = (!a||!b)
                 * !(a||b) = (!a&&!b)
                 */

                enterNegation();
                /**
                 * Third step of the algorithm:
                 *  distribute the || and && operator
                 * (a || (b&&c)) = (a||b) && (a||c)
                 * ((a&&b) || c) = (a || c) && (b||c)
                 */

                distributeOperator();

            }
        }
        else
            throw new RuntimeException("Formula:: Impossible to convert ltl "
                    + "formula to CNF form");

    }

    private void removeImpEqu() {
        if (!isAtomic_){
            switch (operator_.getTag()){
                case (Tag.IMPLIES):
                    operator_ = new Operator(Tag.S_OR);
                    leftFormula_ = new Formula(leftFormula_, new Operator(Tag.S_NOT));
                    leftFormula_.removeImpEqu();
                    rightFormula_.removeImpEqu();
                    break;
                case (Tag.EQUIVALENCE):
                    Formula saveLeft = new Formula(leftFormula_);
                    operator_ = new Operator(Tag.S_AND);
                    leftFormula_ = new Formula(new Formula(leftFormula_,new Operator(Tag.S_NOT)),
                            rightFormula_,new Operator(Tag.S_OR));
                    rightFormula_ = new Formula(saveLeft,
                            new Formula(rightFormula_, new Operator(Tag.S_NOT)),
                            new Operator(Tag.S_OR));
                    leftFormula_.removeImpEqu();
                    rightFormula_.removeImpEqu();
                    break;
                default:
                    if(operator_.isUnary())
                        rightFormula_.removeImpEqu();
                    else{
                        leftFormula_.removeImpEqu();
                        rightFormula_.removeImpEqu();
                    }
            }
        }
    }

    private void enterNegation()  {
        if (!isAtomic_){
            if (operator_.getTag() == Tag.NOT ){
                if (!rightFormula_.isAtomic_){
                    switch(rightFormula_.getOperator().getTag()){
                        case (Tag.AND):
                            operator_ = new Operator(Tag.S_OR);
                            leftFormula_ = new Formula(rightFormula_.getLeftF(),new Operator(Tag.S_NOT));
                            rightFormula_ = new Formula(rightFormula_.getRightF(), new Operator(Tag.S_NOT));
                            leftFormula_.enterNegation();
                            rightFormula_.enterNegation();
                            break;
                        case (Tag.OR):
                            operator_ = new Operator(Tag.S_AND);
                            leftFormula_ = new Formula(rightFormula_.getLeftF(),new Operator(Tag.S_NOT));
                            rightFormula_ = new Formula(rightFormula_.getRightF(), new Operator(Tag.S_NOT));
                            leftFormula_.enterNegation();
                            rightFormula_.enterNegation();
                            break;
                        //There is no other case
                    }
                }
            }
            else{
                leftFormula_.enterNegation();
                rightFormula_.enterNegation();
            }
        }
    }

    private void distributeOperator()  {
        if (!isAtomic_){
            //(a || (b&&c)) = (a||b) && (a||c)
            if (!rightFormula_.isAtomic_ && !rightFormula_.getOperator().isUnary()){
                switch (operator_.getTag()){
                    case (Tag.AND):
                        leftFormula_.distributeOperator();
                        rightFormula_.distributeOperator();
                        break;
                    case (Tag.NOT):
                        rightFormula_.distributeOperator();
                        break;
                    case (Tag.OR):
                        operator_ = new Operator(Tag.S_AND);
                        Formula a = new Formula (leftFormula_);
                        Formula b = new Formula(rightFormula_.getLeftF());
                        Formula c = new Formula(rightFormula_.getRightF());

                        leftFormula_ = new Formula (a,b,new Operator(Tag.S_OR));
                        rightFormula_ = new Formula(a, c, new Operator(Tag.S_OR));

                        leftFormula_.distributeOperator();
                        rightFormula_.distributeOperator();

                        break;
                }
            }
            
            //((a&&b) || c) = (a || c) && (b||c)
            else if (!leftFormula_.isAtomic_ && !leftFormula_.getOperator().isUnary()){
                switch (operator_.getTag()){
                    case (Tag.AND):
                        leftFormula_.distributeOperator();
                        rightFormula_.distributeOperator();
                        break;
                    case (Tag.NOT):
                        rightFormula_.distributeOperator();
                        break;
                    case (Tag.OR):
                        operator_ = new Operator(Tag.S_AND);
                        Formula a = new Formula (leftFormula_.getLeftF());
                        Formula b = new Formula (leftFormula_.getRightF());
                        Formula c = new Formula (rightFormula_);

                        leftFormula_ = new Formula (a,c,new Operator(Tag.S_OR));
                        rightFormula_ = new Formula(b, c, new Operator(Tag.S_OR));

                        leftFormula_.distributeOperator();
                        rightFormula_.distributeOperator();

                        break;
                }
            }
        }
    }

    /**
     * This function convert the atomic proposition to an other representation.
     * This representation is defined in convertTable. The format for convertTable
     * must be : 
     * key : String value : String
     * @param convertTable
     */

    public void convert (Hashtable convertTable){
        if (isAtomic()){
            proposition_ = (String) convertTable.get(proposition_);
        }
        else if (leftFormula_ == null){
            rightFormula_.convert(convertTable);
        }
        else{
            leftFormula_.convert(convertTable);
            rightFormula_.convert(convertTable);
        }
    }

    //*********************** DIVERSE METHOD *********************//

    public File getCnfFile() throws IOException {
        convert2CNF();
        if (isCNF()){
            initNbreVar();
            CnfIterator iter = new CnfIterator(this);
            File cnf = new File ("formula/formula.cnf");
            FileWriter fw = new FileWriter(cnf);
            String str = "p cnf "+getNbreVar()+" "+getNbreClauses()+"\n";
            fw.write("p cnf "+getNbreVar()+" "+getNbreClauses()+"\n");
            fw.write(iter.getClause().toCnfString()+" 0\n");

            while (iter.hasNext()){
                iter.next();
                fw.write(iter.getClause().toCnfString()+" 0\n");
            }
            fw.close();

            return cnf;
        }
        else
            throw new RuntimeException("Formula :: Try to write a cnf file"
                    + " with a non cnf formula");
    }

    public void initNbreVar(){
        nbreVar_ = initVar(new Hashtable());
    }

    private int initVar(Hashtable variables){
        if (isAtomic_){
            if (variables.get(proposition_) == null){
                variables.put(proposition_,(int) variables.size()+1);
                numVar_ = variables.size();
            }
            else
                numVar_ = (Integer) variables.get(proposition_);
            return variables.size();
        }
        else if (leftFormula_==null)
            return rightFormula_.initVar(variables);
        else{
            leftFormula_.initVar(variables);
            return rightFormula_.initVar(variables);
        }
    }

    //*********************** NuGat method **********************//

    public Node encFormula( NuGatInterface nugat,
            Hashtable smvMapTable) {
        nugat_ = nugat;
        smvMapTable_ = smvMapTable;
        return encFormula();
    }

    /**
     * This function return the corresponding NuGat node for the formula
     * @param formula
     * @return
     * @throws IOException
     */

    private Node encFormula() {
        if (isAtomic()){
            if (isTrue())
                return new Node(nugat_.TRUEEXP, Pointer.NULL, Pointer.NULL, nugat_);
            else if (isFalse())
                return new Node(nugat_.FALSEEXP, Pointer.NULL, Pointer.NULL, nugat_);
            else if (isInteger()){
                String nbre = toString();
                int number = Integer.parseInt(nbre);
                return new Node(nugat_.NUMBER,Pointer.createConstant(number),Pointer.NULL,
                        nugat_);
            }
            else {
                Node atomicProp = (Node) smvMapTable_.get(toString());
                if (atomicProp != null)
                    return atomicProp;
                else{
                    return new Node (nugat_.ATOM,nugat_.find_string(proposition_), 
                            Pointer.NULL, nugat_); 
                }
            }
        }
        else if (getOperator().isUnary()){
            Operator operator = getOperator();
            operator.setNugat(nugat_);
            int op = operator.encOp();
            Formula right = getRightF();
            right.setNugatInterface(nugat_);
            right.setSmvMapTable(smvMapTable_);
            Node left = right.encFormula();
            return new Node(op,left.ptr(),Pointer.NULL,nugat_);
        }
        else{
            Operator operator = getOperator();
            operator.setNugat(nugat_);
            int op = operator.encOp();
            Formula leftF = getLeftF();
            leftF.setNugatInterface(nugat_);
            leftF.setSmvMapTable(smvMapTable_);
            Node left = leftF.encFormula();
            Formula rightF = getRightF();
            rightF.setNugatInterface(nugat_);
            rightF.setSmvMapTable(smvMapTable_);
            Node right = rightF.encFormula();
            return new Node(op,left.ptr(),right.ptr(),nugat_);
        }
    }

}
